Nuprl Lemma : minus_thru_mul
13,42
postcript
pdf
a
,
b
:
. (-(
a
*
b
)) = ((-
a
) *
b
)
latex
Up
int
2
,
int
2
Definitions
t
T
,
x
:
A
.
B
(
x
)
origin
a, b:
. (-(a * b)) = ((-a) * b) a, b:. (-(a * b)) = ((-a) * b) 
Tx:A. B(x)